Calculus of Constructions
#Fleeting_Notes
Calculus of Constructions(
CoC
)
端的に表しすぎると下記で構成されるはず
単純型付きラムダ計算
+
依存型
+
型構築子
+
ポリモーフィズム
(
多相型
)
ラムダ・キューブ
でCoCにどうやって至るか(?)が表されている
CoCに
帰納型
を加えると
Calculus of Inductive Constructions(CIC)
になる
確認用
Q. Calculus of Constructions
関連
『The Calculus of Constructions』
Thierry Coquand and G ́erard Huet. The Calculus of Constructions. PhD thesis, INRIA, 1986.
調査用
Google.icon
Calculus of Constructions(日)
Google.icon
Calculus of constructions(英)
Wikipedia.icon
Calculus of Constructions - Wikipedia(日)
Calculus of Constructions(検索) - Wikipedia(日)
Wikipedia.icon
Calculus of constructions - Wikipedia(英)
Calculus of constructions(検索) - Wikipedia(英)